Nuprl Lemma : csupdate-from_wf
11,40
postcript
pdf
Cmd
:Type,
x
:chain_sys(
Cmd
). (
csupdate?(
x
))
(csupdate-from(
x
)
Id)
latex
Definitions
s
=
t
,
t
T
,
True
,
Type
,
Id
,
type
List
,
x
:
A
B
(
x
)
,
P
Q
,
False
,
chain
sys
ind
csupdate
compseq
tag
def
,
b
,
csupdate?(
x
)
,
chain
sys
ind
csinput
compseq
tag
def
,
x
:
A
B
(
x
)
,
left
+
right
,
chain_sys(
Cmd
)
,
csupdate-from(
x
)
,
x
:
A
.
B
(
x
)
Lemmas
assert
wf
,
csupdate?
wf
,
chain
sys
wf
,
false
wf
,
true
wf
origin
Cmd:Type, x:chain_sys(Cmd). (
csupdate?(x)) 
(csupdate-from(x) 
Id) Cmd:Type, x:chain_sys(Cmd). (csupdate?(x)) (csupdate-from(x) Id) T
B(x) Qb
B(x)x:A. B(x)